es:event_system{i:l}, e:es-E(es). sqequal([e, e]; cons(e; [])) 

latex

Definitions	x:A. B(x), [e, e'], t  T, l_all(L; T; x.P(x)), x(s), P  Q, prop{i:l}, A, sq_type(T), guard(T), False, append(as; bs), filter(P; l), Y, reduce(f; k; as), if b then t else f fi , tt, ff, P  Q, P  Q, P  Q, , Unit,
Lemmas	filter append, es-ble wf, es-before wf, es-E wf, event system wf, filter is nil, not functionality wrt iff, assert wf, es-le wf, assert-es-ble, l member wf, member-es-before, es-locl transitivity2, es-locl irreflexivity, filter wf, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, es-le weakening eq